Inference at * 1 
Iof proof for Lemma connex iff trichot:



  T:Type, R:(TT).
  (a, b:T. Dec(R(a,b)))
   (Connex(T;x,y.R(x,y))
    (a, b:T.
    strict_part(x,y.R(x,y);a;b)
     Symmetrize(x,y.R(x,y);a;b)
     strict_part(x,y.R(x,y);b;a))) 

latex

 by ((((Unfolds ``connex strict_part symmetrize`` 0) 
CollapseTHEN (GenRepD))) 
CollapseTHENA (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 1. T : Type
C1: 2. R : TT
C1: 3. a, b:T. Dec(R(a,b))
C1: 4. x, y:T. R(x,y)  R(y,x)
C1: 5. a : T
C1: 6. b : T
C1:   (R(a,b) & (R(b,a)))  (R(a,b) & R(b,a))  (R(b,a) & (R(a,b)))
C2: 

C2: 1. T : Type
C2: 2. R : TT
C2: 3. a, b:T. Dec(R(a,b))
C2: 4. a, b:T. (R(a,b) & (R(b,a)))  (R(a,b) & R(b,a))  (R(b,a) & (R(a,b)))
C2: 5. x : T
C2: 6. y : T
C2:   R(x,y)  R(y,x)
C.

Definitions	t  T, P  Q, P & Q, Symmetrize(x,y.R(x;y);a;b), strict_part(x,y.R(x;y);a;b), P  Q, Connex(T;x,y.R(x;y)), P  Q, x(s1,s2), P  Q, , x:A. B(x)
Lemmas	decidable wf, not wf